Nuprl Lemma : eq_ds_wf
0,22
postcript
pdf
A
:Type,
d
:DS(
A
),
a
:
A
,
x
,
y
:dstype(
A
;
d
;
a
).
x
=
y
latex
Definitions
x
=
y
,
dseq(
d
;
a
)
,
dstype(
TypeNames
;
d
;
a
)
,
DS(
A
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
discrete
struct
wf
,
dstype
wf
,
dseq
wf
origin
A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). x = y 
A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). x = y x:A. B(x) T